STM: action wf

ABS: null

STM: null-action wf

ABS: doact(k;v)

STM: doact wf

ABS: w-action-dec(TA;M;i)

STM: w-action-dec wf

ABS: w-kindtype(TA;M;i)

ABS: w-automaton(T;TA;M)

STM: w-automaton wf

ABS: NullMachine

STM: w-null wf

ABS: World

STM: world wf

ABS: w.T

STM: w-T wf

ABS: w.TA

STM: w-TA wf

ABS: w.M

STM: w-M wf

ABS: vartype(i;x)

STM: w-vartype wf

ABS: Action(i)

STM: w-action wf

ABS: isnull(a)

STM: w-isnull wf

ABS: kind(a)

STM: w-kind wf

ABS: valtype(i;a)

STM: w-valtype wf

ABS: val(a)

STM: w-val wf

ABS: isrcv(l;a)

STM: w-isrcvl wf

STM: assert-w-isrcvl

ABS: Msg

STM: w-Msg wf

ABS: s(i;t).x

STM: w-s wf

ABS: a(i;t)

STM: w-a wf

ABS: m(i;t)

STM: w-m wf

ABS: onlnk(l;mss)

STM: w-onlnk wf

STM: w-onlnk-wf2

STM: w-onlnk-m

ABS: withlnk(l;mss)

STM: w-withlnk wf

ABS: w-tagged(tg;mss)

STM: w-tagged wf

ABS: m(l;t)

STM: w-ml wf

ABS: snds(l;t)

STM: w-snds wf

ABS: rcvs(l;t)

STM: w-rcvs wf

ABS: queue(l;t)

STM: w-queue wf

STM: w-queue-wf2

ABS: msg(a)

STM: w-msg wf

ABS: w-machine(w;i)

STM: w-machine wf

ABS: w-atom-constraint(w)

STM: w-atom-constraint wf

ABS: w-machine-constraint(w)

STM: w-machine-constraint wf

ABS: w-machine-independent(w;i;k;x)

STM: w-machine-independent wf

ABS: FairFifo

STM: fair-fifo wf

ABS: E

STM: w-E wf

ABS: p = q

STM: w-eq-E wf

STM: assert-w-eq-E

STM: assert-w-eq-E-iff

ABS: loc(e)

STM: w-loc wf

ABS: act(e)

STM: w-act wf

STM: w-act-not-null

ABS: kind(e)

STM: w-ekind wf

ABS: V(i;k)

STM: w-V wf

ABS: val(e)

STM: w-eval wf

ABS: time(e)

STM: w-time wf

STM: w-a-not-null

ABS: (x when e)

STM: w-when wf

ABS: (x after e)

STM: w-after wf

ABS: w-pred(w;e)

STM: w-pred wf

STM: w-pred-wf2

ABS: e <loc e'

STM: w-locl wf

ABS: sends(l;e)

STM: w-sends wf

ABS: match(l;t;t')

STM: w-match wf

STM: assert-w-match

STM: w-match-exists

STM: better-w-match-exists

STM: w-match-unique

STM: w-match-property

STM: w-match-member-property

ABS: sender(e)

STM: w-sender wf

ABS: w-info(w;e)

STM: w-info wf

STM: w-loc-lemma

STM: w-loc-w-pred

STM: w-loc-pred

STM: w-loc-rcv

STM: w-loc-sender

STM: w-pred-decreases

STM: w-pred-bound

STM: w-pred!-decreases

STM: w-cless-loc

STM: w-cless-decreases

ABS: w_locl(w;x;y)

STM: w locl wf

STM: w locl-lemma

ABS: w_locle(w;x;y)

STM: w locle wf

STM: w locle-lemma

STM: w-snd-rcv

STM: w-match-sender

STM: w-order-axioms

STM: w-kind-lemma

STM: w-stutter

STM: w-first-null

STM: w-pred-null

STM: w-when-after

ABS: state_when(e)

STM: w state when wf

STM: w-state-when

STM: w-when-lemma

STM: w-when-lemma2

ABS: state_after(e)

STM: w state after wf

STM: w-state-after

STM: w-after-lemma

STM: w-after-lemma2

STM: w-rcv-msg

ABS: w_sends(e;l)

STM: w sends wf

ABS: index(e)

STM: w-index wf

ABS: e <c e'

STM: w-causl wf

STM: w-causl-time

STM: w-locl-iff

STM: w-E sq

STM: world-es-val

STM: world-es-atom

ABS: ES(the_w)

STM: w-es wf

STM: w-sends-reliable

STM: w-sends-nil

STM: w-sends-fifo1

STM: w-sends-fifo

STM: w-sends-msg

STM: no repeats eventlist

STM: w-sends-lemma

STM: w sends-wf2

STM: mlnk-hd-w-queue

STM: es-valtype-w-valtype